A, B:Type, xs:(A List), ys:(B List), x:A, y:B. (<x, y>  zip(xs;ys))  {(x  xs) & (y  ys)} 

latex

ProofTree

Definitions

t  T, type List, x:AB(x), x:A  B(x), (x  l), P & Q, {T}, P  Q, x:A. B(x), Type, <a, b>, tl(l), n - m, if a<b then c else d, i <z j, b, i z j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , nth_tl(n;as), hd(l), l[i], s = t, n+m, rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, ||as||, a < b, A, A  B, , {x:A| B(x)} , , [], False, P  Q, [car / cdr], left + right, P  Q, zip(as;bs), , P  Q, x. t(x), t.1, t.2

Lemmas

pi2 wf, pi1 wf, and functionality wrt iff, cons member, zip wf, nil member, l member wf